Modern design and problem solving endeavors have become increasingly large and complex, often involving collaborations of many individuals working toward a common goal. Consequently, computers have been used to assist individuals and teams in performing and managing such projects. There are numerous limitations of these existing applications of computers, however, and various important challenges of design and problem solving endeavors remain unassisted by computers.
Large-scale collaborative projects involve many people reasoning toward the solution of a common problem over an extended period of time. The design and construction of a product, whether an automobile, a building, or a complex hardware or software system, involves a multi-disciplinary team of clients and engineers working toward a common goal. Such distributed reasoning projects frequently yield less than optimal results, or even flounder, for lack of techniques for structuring and recording the complex rationales that drive the evolution of the design over the course of the project. Even when a successful outcome is achieved, later modification of the product is often hampered by the absence of an easily understood record of these rationales.
Most reasoning and design problems require the marshaling, manipulation and communication of information represented in a wide variety of formats. For example, in addition to circuit diagrams an engineering team may use state machine diagrams, timing diagrams and logic ladder diagrams, together with algebraic or natural language specifications of the desired input/output behavior, in order to produce a design that meets the client's needs. Until recently, theoretical accounts of reasoning have limited themselves to homogeneous linguistic reasoning, that is, reasoning in which all information is represented in the form of sentences of some language, either natural or formal. This limitation presents a major obstacle to the application of insights about the structure of reasoning to real-world, collaborative problem solving.
Graphical editing programs, such as computer aided design (CAD) and computer aided architectural design (CAAD) programs, permit the creation and modification of graphical representations such as mechanical drawings, floor plans, schematics, and the like. Typically, a graphical editing program maintains, at any given time, a single internal graphical data structure that is successively modified during the course of editing. Some graphical editing programs temporarily store a small number of prior modifications to the current representation. If a mistake is made during a current editing session, an "undo" feature can be used to retract the most recent modification and revert to an earlier version of the representation. These prior modifications, however, are lost when the program closes the representation file, and are not, therefore, part of the stored graphical data structure itself. It should also be noted that this "undo" feature only allows reverting backward in time through a linear historical sequence of edits. Moreover, if a large project involves several distinct but related graphical representations, such as distinct versions of the same drawing, these programs store them as separate, unrelated files.
Version control systems (VCSs) have been developed to maintain and navigate through distinct versions of files. These files include, for example, the source code of computer programs as well as files containing other forms of data. The purpose of a version control system is to maintain a historical record of successive versions of a document and to decrease the likelihood of inconsistent changes being made by multiple users. Version control systems generally accomplish this goal by requiring that a file be checked out before a user can change it. When a document is checked out, the user usually receives a modifiable copy of the most recent version of the document. After the user has made changes, the modified version is checked in and becomes the most recent version. The VCS maintains previous versions as well as the new version, and records the historical relationship between them. In some cases, the VCS may allow multiple users to check out and modify a file independently. If the modifications are consistent in the sense that they modify different parts of the file, the system may allow an automatic merge of the two versions that incorporates both sets of changes. In no case, however, does a VCS permit a prior version of a file to be directly altered. Instead, the prior version is always preserved as part of a historical record and any alterations based on the prior version of the file are part of a new file. In addition, a VCS never permits alterations to the relationships between existing files. It only permits the addition of a new version of a file and relates it to the existing version upon which it is based. A VCS is also characterized by the fact that any file that has not been checked out is available for further editing at any point in time. It should also be noted that a VCS separately tracks the histories of different files. The version history of one file, therefore, will normally have a structure unrelated to the version history of another file. Moreover, if the two files represent distinct but related parts of a common project or reasoning task, such relations between files are not represented as part of the version history of each file.
Programs have been developed to assist users in correctly constructing and recording certain reasoning tasks. These programs, however, are typically limited to very rigorous forms of reasoning using very constrained forms of symbolic representation. Current proof software, for example, permits the creation and recording of proofs that preserve the logical structure and dependencies between sentential propositions used in a piece of reasoning. Existing proof software only permits a single, sentential form of representation to be associated with each step of the proof structure. In general, these sentential forms of representation are sentences drawn from one of the formal, symbolic languages developed in mathematical logic (e.g. "propositional logic," "first-order logic," "second-order logic," "predicate calculus," and "functional calculus"). These sentences must conform to exacting syntactical rules. In addition, the relationships between the sentences in the proof structure must conform to rigorous logical rules. Consequently, these programs are limited to assisting in only the most rigorous problem solving tasks that can be unambiguously and completely represented in a formal symbolic language. In short, they are not useful for the vast majority of problem solving tasks.
Hyperproof, a proof software program designed for teaching rigorous deductive reasoning, supports reasoning about a single, highly constrained "blocks world" graphical representation, i.e. a graphical representation of a grid upon which may be placed one of a few types of predefined geometrical objects. Hyperproof also constrains the editing of any blocks world diagram to edits that restrict predefined attributes of the blocks to specific values. In order to make tractable the problem of supporting rigorous reasoning about a graphical representation, Hyperproof is limited to providing support for a simple and highly constrained graphical representation of a blocks world which cannot be extended in any way through the course of the reasoning process. It does not provide support for general purpose reasoning tasks because it does not support reasoning involving multiple graphical representations, arbitrary types of graphical representations, or graphical representations that can be extended throughout the course of the reasoning process. Consequently, the program has extremely limited practical utility outside the context of teaching deductive reasoning.